(declare-fun T4@506184 () (_ BitVec 32))
(declare-fun T4@16 () (_ BitVec 32))
(declare-fun T4@506232 () (_ BitVec 32))
(declare-fun T4@506216 () (_ BitVec 32))
(declare-fun T1@506668 () (_ BitVec 8))
(declare-fun T1@506511 () (_ BitVec 8))
(assert (let ((?x84 (bvadd (bvadd (bvadd T4@16 (_ bv28 32)) (bvmul (_ bv4294967295 32) T4@506184)) (_ bv4 32)))) (let ((?x7 (bvadd (bvadd (_ bv0 32) (bvmul (_ bv4294967295 32) (bvadd (bvadd T4@506216 ?x84) (_ bv1228 32)))) (bvadd T4@506232 ?x84)))) (not (bvsle (bvadd (_ bv0 32) (bvmul (_ bv4294967295 32) ?x7)) (_ bv8 32))))))
(assert (= (_ bv46 8) (bvadd (bvadd T1@506511 (_ bv46 8)) T1@506668)))
(assert (= (_ bv46 8) (bvadd (bvadd T1@506511 (_ bv46 8)) T1@506668)))
(assert (= (_ bv46 8) (bvadd (bvadd T1@506511 (_ bv46 8)) T1@506668)))
(check-sat)
